$\forall$$T$:Type, $L$:($T$ List), $R$:(\{$x$:$T$$\mid$ ($x$ $\in$ $L$)\} $\rightarrow$es\_realizer\{i:l\}), ${\it es}$:event\_system\{i:l\}. \\[0ex]R{-}consistent(Rall($L$; $x$.$R$($x$)); ${\it es}$) $\Leftarrow\!\Rightarrow$ l\_all($L$; $T$; $x$.R{-}consistent($R$($x$); ${\it es}$))